Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    (x - y) + z  → (x + z) - y
2:    (x + y) - y  → x
There are 2 dependency pairs:
3:    (x - y) +# z  → (x + z) -# y
4:    (x - y) +# z  → x +# z
The approximated dependency graph contains one SCC: {4}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006